$\forall$${\it es}$:event\_system\{i:l\}, $e$:es{-}E(${\it es}$), $x$,${\it free}$:Id.
\\[0ex]es{-}dtype(${\it es}$; loc($e$); $x$; Id) $\Rightarrow$ (f{-}round\{i:l\}($x$; ${\it free}$; ${\it es}$; $e$) $\in$ $\mathbb{N}$)